Nuprl Lemma : assoced_elim 11,40

a,b:. assoced(ab ((a = b (a = (-b))) 
latex


Definitionst  T, assoced(ab), x:AB(x), P  Q, P  Q, P  Q, P  Q, pm_equal(ij), P  Q, prop{i:l}
Lemmasassoc reln, iff functionality wrt iff, pm equal wf, divides wf

origin